Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(b) → A__B
A__A1A__A
MARK(k) → A__K
A__A1A__H(a__f(a__a), a__f(a__b))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A1
A__A1A__B
A__AA__C
A__AA__D
MARK(A) → A__A1
A__H(X, X) → A__K
A__A1A__F(a__b)
A__A1A__F(a__a)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__BA__C
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
MARK(a) → A__A
MARK(c) → A__C
MARK(f(X)) → A__F(mark(X))
MARK(d) → A__D
A__BA__D

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(b) → A__B
A__A1A__A
MARK(k) → A__K
A__A1A__H(a__f(a__a), a__f(a__b))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A1
A__A1A__B
A__AA__C
A__AA__D
MARK(A) → A__A1
A__H(X, X) → A__K
A__A1A__F(a__b)
A__A1A__F(a__a)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__BA__C
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
MARK(a) → A__A
MARK(c) → A__C
MARK(f(X)) → A__F(mark(X))
MARK(d) → A__D
A__BA__D

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 12 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
QDP
          ↳ RuleRemovalProof

Q DP problem:
The TRS P consists of the following rules:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__A1A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A1
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(A) → A__A1
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
A__A1A__F(a__b)
A__A1A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(g(X1, X2, X3)) → MARK(X1)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
MARK(A) → A__A1
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)


Used ordering: POLO with Polynomial interpretation [25]:

POL(A) = 1   
POL(A__A1) = 0   
POL(A__F(x1)) = 2·x1   
POL(A__G(x1, x2, x3)) = x1 + x2 + x3   
POL(A__H(x1, x2)) = x1 + x2   
POL(A__Z(x1, x2)) = x1 + x2   
POL(MARK(x1)) = x1   
POL(a) = 0   
POL(a__A) = 1   
POL(a__a) = 0   
POL(a__b) = 0   
POL(a__c) = 0   
POL(a__d) = 0   
POL(a__f(x1)) = 2·x1   
POL(a__g(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(a__h(x1, x2)) = 1 + x1 + 2·x2   
POL(a__k) = 0   
POL(a__z(x1, x2)) = x1 + x2   
POL(b) = 0   
POL(c) = 0   
POL(d) = 0   
POL(e) = 0   
POL(f(x1)) = 2·x1   
POL(g(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(h(x1, x2)) = 1 + x1 + 2·x2   
POL(k) = 0   
POL(l) = 0   
POL(m) = 0   
POL(mark(x1)) = x1   
POL(z(x1, x2)) = x1 + x2   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ RuleRemovalProof
QDP
              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

A__F(X) → A__Z(mark(X), X)
A__A1A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A1
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__A1A__F(a__b)
A__A1A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
QDP
                    ↳ QDPOrderProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A__F(X) → A__Z(mark(X), X)
MARK(f(X)) → A__F(mark(X))
A__F(X) → MARK(X)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__Z(e, X) → MARK(X)

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


MARK(f(X)) → A__F(mark(X))
MARK(f(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.

A__F(X) → A__Z(mark(X), X)
A__F(X) → MARK(X)
MARK(z(X1, X2)) → MARK(X1)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__Z(e, X) → MARK(X)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( c ) =
/0\
\0/

M( a ) =
/0\
\0/

M( a__b ) =
/0\
\0/

M( z(x1, x2) ) =
/0\
\0/
+
/01\
\10/
·x1+
/10\
\01/
·x2

M( a__h(x1, x2) ) =
/0\
\0/
+
/00\
\10/
·x1+
/00\
\00/
·x2

M( e ) =
/0\
\0/

M( k ) =
/1\
\0/

M( mark(x1) ) =
/0\
\0/
+
/10\
\01/
·x1

M( d ) =
/0\
\0/

M( A ) =
/0\
\0/

M( a__d ) =
/0\
\0/

M( a__A ) =
/0\
\0/

M( a__k ) =
/1\
\0/

M( a__z(x1, x2) ) =
/0\
\0/
+
/01\
\10/
·x1+
/10\
\01/
·x2

M( m ) =
/0\
\0/

M( a__c ) =
/0\
\0/

M( f(x1) ) =
/0\
\1/
+
/11\
\11/
·x1

M( l ) =
/0\
\0/

M( a__g(x1, ..., x3) ) =
/0\
\0/
+
/00\
\00/
·x1+
/00\
\00/
·x2+
/00\
\00/
·x3

M( a__f(x1) ) =
/0\
\1/
+
/11\
\11/
·x1

M( h(x1, x2) ) =
/0\
\0/
+
/00\
\10/
·x1+
/00\
\00/
·x2

M( g(x1, ..., x3) ) =
/0\
\0/
+
/00\
\00/
·x1+
/00\
\00/
·x2+
/00\
\00/
·x3

M( b ) =
/0\
\0/

M( a__a ) =
/0\
\0/

Tuple symbols:
M( A__Z(x1, x2) ) = 1+
[0,0]
·x1+
[1,1]
·x2

M( MARK(x1) ) = 1+
[1,1]
·x1

M( A__F(x1) ) = 1+
[1,1]
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

a__aa__c
a__ba__c
a__cl
a__ba__d
a__km
a__kl
a__ce
a__aa__d
a__dm
mark(a) → a__a
mark(A) → a__A
mark(c) → a__c
mark(b) → a__b
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__Aa__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(e) → e
mark(l) → l
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(d) → a__d
mark(k) → a__k
a__kk
a__z(X1, X2) → z(X1, X2)
a__cc
a__dd
a__aa
a__bb
mark(m) → m
a__AA
a__g(X1, X2, X3) → g(X1, X2, X3)
a__h(X1, X2) → h(X1, X2)
a__f(X) → f(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ DependencyGraphProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A__F(X) → A__Z(mark(X), X)
MARK(z(X1, X2)) → MARK(X1)
A__F(X) → MARK(X)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ DependencyGraphProof
QDP
                            ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MARK(z(X1, X2)) → MARK(X1)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
QDP
                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

A__A1A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A1

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A__A1A__H(a__f(a__a), a__f(a__b)) at position [] we obtained the following new rules:

A__A1A__H(f(a__a), a__f(a__b))
A__A1A__H(a__f(a__a), f(a__b))
A__A1A__H(a__f(a__a), a__f(a__c))
A__A1A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A1A__H(a__f(a__d), a__f(a__b))
A__A1A__H(a__f(a__a), a__f(b))
A__A1A__H(a__f(a), a__f(a__b))
A__A1A__H(a__f(a__a), a__f(a__d))
A__A1A__H(a__f(a__c), a__f(a__b))
A__A1A__H(a__f(a__a), a__z(mark(a__b), a__b))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ Narrowing
QDP
                        ↳ QDPOrderProof
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

A__A1A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A1A__H(a__f(a__d), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A1
A__A1A__H(a__f(a__a), a__f(a__d))
A__A1A__H(a__f(a__c), a__f(a__b))
A__A1A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A1A__H(f(a__a), a__f(a__b))
A__A1A__H(a__f(a__a), f(a__b))
A__A1A__H(a__f(a__a), a__f(a__c))
A__A1A__H(a__f(a__a), a__f(b))
A__A1A__H(a__f(a), a__f(a__b))

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


A__A1A__H(a__f(a__a), a__f(a__c))
The remaining pairs can at least be oriented weakly.

A__A1A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A1A__H(a__f(a__d), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A1
A__A1A__H(a__f(a__a), a__f(a__d))
A__A1A__H(a__f(a__c), a__f(a__b))
A__A1A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A1A__H(f(a__a), a__f(a__b))
A__A1A__H(a__f(a__a), f(a__b))
A__A1A__H(a__f(a__a), a__f(b))
A__A1A__H(a__f(a), a__f(a__b))
Used ordering: Combined order from the following AFS and order.
A__A1  =  A__A1
A__H(x1, x2)  =  x2
a__z(x1, x2)  =  x2
mark(x1)  =  x1
a__a  =  a__a
a__f(x1)  =  x1
a__b  =  a__b
a__d  =  a__d
A__G(x1, x2, x3)  =  x1
a__k  =  a__k
d  =  d
a__c  =  a__c
f(x1)  =  x1
b  =  b
a  =  a
l  =  l
m  =  m
e  =  e
A  =  A
a__A  =  a__A
c  =  c
a__h(x1, x2)  =  a__h
a__g(x1, x2, x3)  =  a__g
h(x1, x2)  =  h
g(x1, x2, x3)  =  g
z(x1, x2)  =  x2
k  =  k

Recursive path order with status [2].
Quasi-Precedence:
[aa, a] > [AA^1, ab, ad, ak, d, b, A, aA, ah, ag, h, g, k] > [ac, l, e, c]
[aa, a] > [AA^1, ab, ad, ak, d, b, A, aA, ah, ag, h, g, k] > m

Status:
c: multiset
a: multiset
ab: multiset
ah: []
e: multiset
AA^1: multiset
k: multiset
ag: []
d: multiset
A: multiset
h: []
ad: multiset
aA: multiset
ak: multiset
ac: multiset
m: multiset
l: multiset
g: []
b: multiset
aa: multiset


The following usable rules [17] were oriented:

a__aa__c
a__ba__c
a__cl
a__ba__d
a__km
a__kl
a__ce
a__aa__d
a__dm
mark(a) → a__a
mark(A) → a__A
mark(c) → a__c
mark(b) → a__b
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__Aa__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(e) → e
mark(l) → l
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(d) → a__d
mark(k) → a__k
a__kk
a__z(X1, X2) → z(X1, X2)
a__cc
a__dd
a__aa
a__bb
mark(m) → m
a__AA
a__g(X1, X2, X3) → g(X1, X2, X3)
a__h(X1, X2) → h(X1, X2)
a__f(X) → f(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ QDPOrderProof
QDP
                            ↳ QDPOrderProof
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

A__A1A__H(a__f(a__a), f(a__b))
A__A1A__H(f(a__a), a__f(a__b))
A__A1A__H(a__f(a__d), a__f(a__b))
A__A1A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__A1A__H(a__f(a), a__f(a__b))
A__A1A__H(a__f(a__a), a__f(b))
A__G(d, X, X) → A__A1
A__A1A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A1A__H(a__f(a__c), a__f(a__b))
A__A1A__H(a__f(a__a), a__f(a__d))

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


A__A1A__H(a__f(a__c), a__f(a__b))
The remaining pairs can at least be oriented weakly.

A__A1A__H(a__f(a__a), f(a__b))
A__A1A__H(f(a__a), a__f(a__b))
A__A1A__H(a__f(a__d), a__f(a__b))
A__A1A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__A1A__H(a__f(a), a__f(a__b))
A__A1A__H(a__f(a__a), a__f(b))
A__G(d, X, X) → A__A1
A__A1A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A1A__H(a__f(a__a), a__f(a__d))
Used ordering: Polynomial interpretation [25]:

POL(A) = 1   
POL(A__A1) = 1   
POL(A__G(x1, x2, x3)) = x1   
POL(A__H(x1, x2)) = x1   
POL(a) = 1   
POL(a__A) = 1   
POL(a__a) = 1   
POL(a__b) = 1   
POL(a__c) = 0   
POL(a__d) = 1   
POL(a__f(x1)) = x1   
POL(a__g(x1, x2, x3)) = 1   
POL(a__h(x1, x2)) = 1   
POL(a__k) = 0   
POL(a__z(x1, x2)) = x2   
POL(b) = 1   
POL(c) = 0   
POL(d) = 1   
POL(e) = 0   
POL(f(x1)) = x1   
POL(g(x1, x2, x3)) = 1   
POL(h(x1, x2)) = 1   
POL(k) = 0   
POL(l) = 0   
POL(m) = 0   
POL(mark(x1)) = x1   
POL(z(x1, x2)) = x2   

The following usable rules [17] were oriented:

a__aa__c
a__ba__c
a__cl
a__ba__d
a__km
a__kl
a__ce
a__aa__d
a__dm
mark(a) → a__a
mark(A) → a__A
mark(c) → a__c
mark(b) → a__b
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__Aa__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(e) → e
mark(l) → l
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(d) → a__d
mark(k) → a__k
a__kk
a__z(X1, X2) → z(X1, X2)
a__cc
a__dd
a__aa
a__bb
mark(m) → m
a__AA
a__g(X1, X2, X3) → g(X1, X2, X3)
a__h(X1, X2) → h(X1, X2)
a__f(X) → f(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ QDPOrderProof
QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

A__A1A__H(f(a__a), a__f(a__b))
A__A1A__H(a__f(a__a), f(a__b))
A__A1A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A1A__H(a__f(a__d), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A1
A__A1A__H(a__f(a__a), a__f(b))
A__A1A__H(a__f(a), a__f(a__b))
A__A1A__H(a__f(a__a), a__f(a__d))
A__A1A__H(a__f(a__a), a__z(mark(a__b), a__b))

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


A__A1A__H(a__f(a__c), a__f(a__b))
The remaining pairs can at least be oriented weakly.

A__A1A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A1A__H(a__f(a__d), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A1
A__A1A__H(a__f(a__a), a__f(a__d))
A__A1A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A1A__H(f(a__a), a__f(a__b))
A__A1A__H(a__f(a__a), f(a__b))
A__A1A__H(a__f(a__a), a__f(a__c))
A__A1A__H(a__f(a__a), a__f(b))
A__A1A__H(a__f(a), a__f(a__b))
Used ordering: Polynomial interpretation [25]:

POL(A) = 1   
POL(A__A1) = 1   
POL(A__G(x1, x2, x3)) = x1   
POL(A__H(x1, x2)) = x1   
POL(a) = 1   
POL(a__A) = 1   
POL(a__a) = 1   
POL(a__b) = 1   
POL(a__c) = 0   
POL(a__d) = 1   
POL(a__f(x1)) = x1   
POL(a__g(x1, x2, x3)) = 1   
POL(a__h(x1, x2)) = 1   
POL(a__k) = 0   
POL(a__z(x1, x2)) = x2   
POL(b) = 1   
POL(c) = 0   
POL(d) = 1   
POL(e) = 0   
POL(f(x1)) = x1   
POL(g(x1, x2, x3)) = 1   
POL(h(x1, x2)) = 1   
POL(k) = 0   
POL(l) = 0   
POL(m) = 0   
POL(mark(x1)) = x1   
POL(z(x1, x2)) = x2   

The following usable rules [17] were oriented:

a__aa__c
a__ba__c
a__cl
a__ba__d
a__km
a__kl
a__ce
a__aa__d
a__dm
mark(a) → a__a
mark(A) → a__A
mark(c) → a__c
mark(b) → a__b
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__Aa__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(e) → e
mark(l) → l
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(d) → a__d
mark(k) → a__k
a__kk
a__z(X1, X2) → z(X1, X2)
a__cc
a__dd
a__aa
a__bb
mark(m) → m
a__AA
a__g(X1, X2, X3) → g(X1, X2, X3)
a__h(X1, X2) → h(X1, X2)
a__f(X) → f(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ QDPOrderProof
                        ↳ QDPOrderProof
QDP

Q DP problem:
The TRS P consists of the following rules:

A__A1A__H(a__f(a__a), f(a__b))
A__A1A__H(f(a__a), a__f(a__b))
A__A1A__H(a__f(a__a), a__f(a__c))
A__A1A__H(a__f(a__d), a__f(a__b))
A__A1A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__A1A__H(a__f(a), a__f(a__b))
A__A1A__H(a__f(a__a), a__f(b))
A__G(d, X, X) → A__A1
A__A1A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A1A__H(a__f(a__a), a__f(a__d))

The TRS R consists of the following rules:

a__aa__c
a__ba__c
a__ce
a__kl
a__dm
a__aa__d
a__ba__d
a__cl
a__km
a__Aa__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__AA
a__aa
a__bb
a__cc
a__dd
a__kk
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.